fetch or.ax;
assume isblock(a);
tauteq x=a⊃isblock(x) 2;
∀i 3 x;
tauteq ∀x.(isblock(x)⊃x=a) 1 4;
∀e 5 x;
tauteq isblock(x)≡x=a 2 6;
∀i 7 x;
⊃i 2 8;
∧i newax[P←λx.(x=b)];
∧i newaxiom[P←λx.(x=b)];
assume isblock(b);
tauteq x=b⊃isblock(x) 11;
∀i 12 x;
tauteq ∀x.(isblock(x)⊃x=b) 10 13;
⊃i 11 14;
show prf;
taut ∀x.(isblock(x)⊃x=a) ∨ ∀x.(isblock(x)⊃x=b) whichblock 9 15;
cancel;
∀e ↑ x;
tauteq isblock(x)≡x=b 15 11;
∀i 16 x;
⊃i 11 17;
taut ∀x.(isblock(x)≡x=a)∨∀x.(isblock(x)≡x=b) 9 18 whichblock;
show axiom newaxiom;
assume (P(a)∨P(b)) ∧ ∀x.(P(x) ⊃ isblock(x));
taut ∀x.(P(x) ⊃ isblock(x)) 20;
∀e 21 x;
assume ∀x.(isblock(x)≡x=a);
∀e 23 x;
assume P(a);
tauteq isblock(x) ⊃ P(x) 22 24 25;
∀i 26 x;
show prf 19:↑;
⊃i 25 ↑;
⊃i 23 ↑;
⊃i 20 ↑;
assume ∀x.(isblock(x) ≡ x=b);
∀e 31 x;
show prf 19:↑;
assume P(b);
tauteq isblock(x)⊃P(x) 22 32 33;
∀i 34 x;
⊃i 33 35;
⊃i ↑ 31;
cancel;
⊃i 31 ↑;
⊃i 20 ↑;
show prf 19:↑;
taut ((P(a)∨P(b))∧∀x.(P(x)⊃isblock(x))⊃∀x.(isblock(x)⊃P(x)) 19 30 38;
taut (((P(a)∨P(b))∧∀x.(P(x)⊃isblock(x)))⊃∀x.(isblock(x)⊃P(x)) 19 30 38;
taut ((P(a)∨P(b));
taut (P(a)∨P(b))∧∀x.(P(x)⊃isblock(x)) ⊃ ∀x.(isblock(x)⊃P(x)) 19 30 38;
show prf 19:↑;
exit;show proof→foo.assume ∃x.isblock(x);
circumscribe isblock P x in 39;
circumscribe foo isblock P x in 39;
∃e 39 a;
∃e 39 x;
∧i foo[P←λy.y=x];
declare INDVAR y;
∧i foo[P←λy.y=x];